D:Dsys, sched:(Id(?((IdLnk + Id)))), v:(i:IdM(i).(timed)state),
dec:(i,a:IdM(i).state(?if a  dom(M(i).prob) then Outcome else Void fi )),
discrete:(IdId), t:.
Feasible(D)  (d-comp-partial-world(D; v; sched; dec; discrete; t)  World) 

latex

Definitions

Dsys, t  T, Unit, Type, IdLnk, left + right, Id, , x:AB(x), x:A. B(x), M(i), M.(timed)state, Void, ma-prob(M;b), Outcome, b  dom(M.prob), if b then t else f fi , M.state, , Feasible(D), d-comp-partial-world(D; v; sched; dec; discrete; t), World, P  Q, False, A, A  B, , {x:A| B(x)} , d-comp(D; v; sched; dec; d), d-world-state(D;i), #$n, {i..j}, s = t, d-partial-world(D;f;t';s;d), x.A(x), b, , b, (i = j), x:A  B(x), P & Q, P  Q, Atom$n, f(a), M.init(x)?v, timedState(ds), t.1, -n, n+m, a < b, n - m, CV(F), S  T, i  j < k, suptype(S; T)

Lemmas

CV wf, le wf, ma-init-val wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bnot wf, not wf, assert wf, d-partial-world wf, int seg wf, d-world-state wf, d-comp wf2, d-feasible wf, bool wf, ma-st wf, ifthenelse wf, ma-prob-dom wf, p-outcome wf, ma-prob wf, ma-tst wf, d-m wf, Id wf, nat wf, IdLnk wf, unit wf, dsys wf